:- module(timeout).
:- export call_timeout_safe_body / 2.
:- export timeout_body / 8.
:- export timeout_body / 4.
:- export call_timeout_safe / 1.
:- export timeout / 7.
:- export timeout / 3.
:- comment(summary, "Impose time limit for goals").
:- comment(author, "Andrew Cheadle, Joachim Schimpf, IC-Parc").
:- comment(date, "$Date: 2004/11/29 16:36:22 $").
:- comment(copyright, "Imperial College London and Parc Technologies Ltd").
:- comment(call_timeout_safe / 1, [amode : call_timeout_safe(+), args : ["Goal" : "Goal to execute"], summary : "Execute Goal, deferring the execution of an interrupting timeout predicate TimeOutGoal until Goal completes.", resat : "If Goal is resatisfiable.", desc : html("\n<P>\n    Metacall Goal, ensuring that its execution is not interrupted and\n    preemptively aborted by a timeout of the timeout/3 or timeout/7 predicate.\n    If a timeout would have occurred during the execution of Goal, it is\n    effectively deferred until Goal completes.\n<P>\n    The predicate can be used within a computation which is subject to timeouts,\n    to ensure that subgoals which should be executed as an atomic sequence\n    preserve this atomicity at the cost of delaying the execution\n    of TimeOutGoal.\n<P>\n    In all other respects the semantics of call_timeout_safe/1 is the same\n    as call/1.\n    "), see_also : [timeout / 3, timeout / 7], eg : "    ?- timeout(call_timeout_safe((writeln('Goal started'), \n                               sleep(5), \n                               writeln('Goal completed'))),\n            3, writeln('Timeout expired!')).\n    Goal started\n    Goal completed\n    Timeout expired!\n    Yes (0.01s cpu)\n    "]).
:- comment(timeout / 3, [amode : timeout(+, ++, +), args : ["Goal" : "Goal to run", "TimeLimit" : "Time limit of Goal in seconds (integer or float)", "TimeOutGoal" : "Goal to run on expiry of TimeLimit"], summary : "Run the goal Goal for a maximum of TimeLimit seconds.", resat : "If Goal is resatisfiable.", desc : html("\n<P>\n    Goal is executed as if called via call(Goal),\n    but only for a maximum of TimeLimit seconds. If the goal is\n    still executing after TimeLimit, time-out occurs, the execution of the\n    goal is terminated (via exit_block/1) and TimeOutGoal is executed.  If\n    the value of TimeLimit is 0 or 1.0Inf, no timeout is applied to the Goal.\n<P>\n    Note that, if Goal is nondeterministic, execution flow may leave the scope\n    of timeout/3 on success and re-enter on failure. In this case, only time\n    spent within Goal will be counted towards the TimeLimit.\n<P>\n    The predicate is based on the after event timers, so TimeLimit is \n    measured in the timer currently used by after events. The current time\n    used for the associated event timer can be retrieved using\n    statistics(event_time, CurrentTime). The timeout predicate can be used \n    with other after events, and can be nested within itself (i.e. embedded\n    within Goal or TimeOutGoal).\n<P>\n    Note that timeout/3 can be defined in terms of timeout/7 as:\n<PRE>\n    timeout(Goal, TimeLimit, TimeOutGoal) :-\n        timeout(Goal, TimeLimit, TimeOutGoal, all_solution, _, _, _).\n</PRE>\n    "), see_also : [timeout / 7, call_timeout_safe / 1, event_after / 2], eg : "    ?- timeout((repeat,fail), 1.5, writeln(timed-out)). % time-out from infinite loop\n    timed - out\n    Yes (1.51s cpu)\n    "]).
:- comment(timeout / 7, [amode : timeout(+, ++, +, ++, ?, ?, ?), args : ["Goal" : "Goal to run", "TimeLimit" : "Time limit of Goal in seconds (integer or float)", "TimeOutGoal" : "Goal to run on expiry of TimeLimit", "SolutionMode" : "Time limit applies to all solutions or per solution (atom)", "Timer" : "After event timer handle", "DueTime" : "Time at which TimeLimit expires (float)", "TimeRemaining" : "Time remaining until goal would have expired (float)"], summary : "Run the goal Goal for a maximum of TimeLimit seconds.", resat : "If Goal is resatisfiable.", desc : html("\n<P>\n    Goal is executed for a maximum of TimeLimit seconds. If the goal is still\n    executing after TimeLimit, time-out occurs, the execution of the goal is\n    terminated (via exit_block/1) and TimeOutGoal is executed.  If the value\n    of TimeLimit is 0 or 1.0Inf, no timeout is applied to the Goal.\n<P>\n    SolutionMode is one of all_solution or per_solution.  If Goal is\n    resatisfiable, then, having found a solution, the per_solution\n    option reapplies the full value of the originally specified\n    TimeLimit to the resuming Goal.  The all_solution option resumes\n    the Goal with the unelapsed portion of TimeLimit (i.e.  its\n    remainder) as the expiry time, the expiry time therefore remains\n    the same.\n<P>\n    Timer is the after-event handle assigned to this timeout goal. It\n    may be used within Goal to force early expiry of the timeout using:\n    event(Timer). \n<P>\n    DueTime is the time at which TimeLimit expires and the TimeOutGoal is \n    posted. It is instantiated before Goal starts executing and may therefore \n    be used within Goal and TimeOutGoal. DueTime is undefined (and remains\n    uninstantiated) if the per_solution SolutionMode is specified.\n<P>\n    On success, TimeRemaining is the time left until TimeLimit expiry,\n    if Goal completes before then, on timeout, TimeRemaining is 0.0.\n<P>\n    The predicate is based on the after event timers, so TimeLimit is \n    measured in the timer currently used by after events. The current time\n    used for the associated event timer can be retrieved using\n    statistics(event_time, CurrentTime). The timeout predicate can be used \n    with other after events, and can be nested within itself (i.e. embedded\n    within Goal or TimeOutGoal). Within Goal, the remaining time that the Goal\n    has left to run before time-out can be computed using:\n<PRE>\n    RemainingTime is max(0.0, DueTime - statistics(event_time)).\n</PRE>\n    This may be useful for setting up sub-timeouts as a fraction of the\n    total remaining time.\n    "), see_also : [timeout / 3, call_timeout_safe / 1, event_after / 2, event / 1], eg : "    % time-out from infinite loop\n    ?- timeout((repeat,fail), 1.5, writeln(timed-out), \n            all_solution, Timer, Due, Remainder).\n    timed - out\n    Timer = 'EVENT'(16'ed920978)\n    Due = Due\n    Remainder = 0.0\n    Yes (1.51s cpu)\n    "]).
:- comment(call_timeout_safe_body / 2, hidden).
:- comment(timeout_body / 8, hidden).
:- comment(timeout_body / 4, hidden).
